A:MsgA. A ||  

latex

Definitions	x:A. B(x), M1 || M2, , P & Q, M1 ||decl M2, mk-ma, t.1, t.2, Valtype(da;k), Top, t  T, x. t(x), MsgA, x(s)
Lemmas	fpf-empty-compatible-right, Id wf, id-deq wf, fpf-trivial-subtype-top, Knd wf, Kind-deq wf, rationals wf, fpf-cap wf, ma-state wf, bool wf, product-deq wf, pi1 wf, top wf, pi2 wf, IdLnk wf, idlnk-deq wf, rcv wf, finite-prob-space wf, msga wf